| Definitions | (e <loc e'), e c e', e loc e' , sender(e), -n, i  j ,  x.A(x), pred(e), first(e), suptype(S; T), pred!(e;e'), kind(e), loc(e), SWellFounded(R(x;y)),  x:A. B(x), (x  l), |g|, n - m, S  T, n+m, #$n, Outcome, A B, False, {T}, a < b,  , p   q, p  q, p   q, e = e', deq-member(eq;x;L), a = b, a = b, qeq(r;s), q_less(a;b), q_le(r;s), eq_atom$n(x;y), [d], a < b, x f y, a < b, null(as), x =a y, (i = j), i z j, i <z j, p =b q, constant_function(f;A;B), r s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time),  ,  , Msg(M), kindcase(k; a.f(a); l,t.g(l;t) ),  x,y. t(x;y), x. t(x), Knd, EState(T), f(a), EOrderAxioms(E; pred?; info), Id, IdLnk, Unit, EqDecider(T), X(e), E(X), a:A fp B(a), strong-subtype(A;B), f(x)?z, type List, P  Q, P & Q, P Q, {x:A| B(x)} ,  x:A.B(x), Void, if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), Top, tt,  b, (e < e'), t.1, let x,y = A in B(x;y), left + right, x:A  B(x), <a, b>, P Q, prior-state(f;base;X;e),  ,  , e X, prior(X), ff, AbsInterface(A), Type, ES,  b, s = t, A,  x:A. B(x), E, x:A B(x), t T |